$M$.pre($a$,$s$,$v$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$fpf{-}val(IdDeq; 1of(2of(2of(2of($M$)))); $a$; $a$,$P$.($P$($s$,$v$)))